/-
Copyright (c) 2022 Thomas Browning. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Thomas Browning
-/

import group_theory.abelianization
import group_theory.exponent
import group_theory.transfer

/-!
# Schreier's Lemma

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

In this file we prove Schreier's lemma.

## Main results

- `closure_mul_image_eq` : **Schreier's Lemma**: If `R : set G` is a right_transversal
  of `H : subgroup G` with `1 ∈ R`, and if `G` is generated by `S : set G`,
  then `H` is generated by the `set` `(R * S).image (λ g, g * (to_fun hR g)⁻¹)`.
- `fg_of_index_ne_zero` : **Schreier's Lemma**: A finite index subgroup of a finitely generated
  group is finitely generated.
- `card_commutator_le_of_finite_commutator_set`: A theorem of Schur: The size of the commutator
  subgroup is bounded in terms of the number of commutators.
-/

open_locale pointwise

namespace subgroup

open mem_right_transversals

variables {G : Type*} [group G] {H : subgroup G} {R S : set G}

lemma closure_mul_image_mul_eq_top
  (hR : R ∈ right_transversals (H : set G)) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
  (closure ((R * S).image (λ g, g * (to_fun hR g)⁻¹)) : set G) * R = ⊤ :=
begin
  let f : G → R := λ g, to_fun hR g,
  let U : set G := (R * S).image (λ g, g * (f g)⁻¹),
  change (closure U : set G) * R = ⊤,
  refine top_le_iff.mp (λ g hg, _),
  apply closure_induction_right (eq_top_iff.mp hS (mem_top g)),
  { exact ⟨1, 1, (closure U).one_mem, hR1, one_mul 1⟩ },
  { rintros - s hs ⟨u, r, hu, hr, rfl⟩,
    rw show u * r * s = u * ((r * s) * (f (r * s))⁻¹) * f (r * s), by group,
    refine set.mul_mem_mul ((closure U).mul_mem hu _) (f (r * s)).coe_prop,
    exact subset_closure ⟨r * s, set.mul_mem_mul hr hs, rfl⟩ },
  { rintros - s hs ⟨u, r, hu, hr, rfl⟩,
    rw show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹), by group,
    refine set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem _)) (f (r * s⁻¹)).2,
    refine subset_closure ⟨f (r * s⁻¹) * s, set.mul_mem_mul (f (r * s⁻¹)).2 hs, _⟩,
    rw [mul_right_inj, inv_inj, ←subtype.coe_mk r hr, ←subtype.ext_iff, subtype.coe_mk],
    apply (mem_right_transversals_iff_exists_unique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
      (mul_inv_to_fun_mem hR (f (r * s⁻¹) * s)),
    rw [mul_assoc, ←inv_inv s, ←mul_inv_rev, inv_inv],
    exact to_fun_mul_inv_mem hR (r * s⁻¹) },
end

/-- **Schreier's Lemma**: If `R : set G` is a right_transversal of `H : subgroup G`
  with `1 ∈ R`, and if `G` is generated by `S : set G`, then `H` is generated by the `set`
  `(R * S).image (λ g, g * (to_fun hR g)⁻¹)`. -/
lemma closure_mul_image_eq
  (hR : R ∈ right_transversals (H : set G)) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
  closure ((R * S).image (λ g, g * (to_fun hR g)⁻¹)) = H :=
begin
  have hU : closure ((R * S).image (λ g, g * (to_fun hR g)⁻¹)) ≤ H,
  { rw closure_le,
    rintros - ⟨g, -, rfl⟩,
    exact mul_inv_to_fun_mem hR g },
  refine le_antisymm hU (λ h hh, _),
  obtain ⟨g, r, hg, hr, rfl⟩ :=
  show h ∈ _, from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h),
  suffices : (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R),
  { rwa [show r = 1, from subtype.ext_iff.mp this, mul_one] },
  apply (mem_right_transversals_iff_exists_unique_mul_inv_mem.mp hR r).unique,
  { rw [subtype.coe_mk, mul_inv_self],
    exact H.one_mem },
  { rw [subtype.coe_mk, inv_one, mul_one],
    exact (H.mul_mem_cancel_left (hU hg)).mp hh },
end

/-- **Schreier's Lemma**: If `R : set G` is a right_transversal of `H : subgroup G`
  with `1 ∈ R`, and if `G` is generated by `S : set G`, then `H` is generated by the `set`
  `(R * S).image (λ g, g * (to_fun hR g)⁻¹)`. -/
lemma closure_mul_image_eq_top
  (hR : R ∈ right_transversals (H : set G)) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
  closure ((R * S).image (λ g, ⟨g * (to_fun hR g)⁻¹, mul_inv_to_fun_mem hR g⟩) : set H) = ⊤ :=
begin
  rw [eq_top_iff, ←map_subtype_le_map_subtype, monoid_hom.map_closure, set.image_image],
  exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS)),
end

/-- **Schreier's Lemma**: If `R : finset G` is a right_transversal of `H : subgroup G`
  with `1 ∈ R`, and if `G` is generated by `S : finset G`, then `H` is generated by the `finset`
  `(R * S).image (λ g, g * (to_fun hR g)⁻¹)`. -/
lemma closure_mul_image_eq_top' [decidable_eq G] {R S : finset G}
  (hR : (R : set G) ∈ right_transversals (H : set G)) (hR1 : (1 : G) ∈ R)
  (hS : closure (S : set G) = ⊤) :
  closure ((((R * S).image (λ g, ⟨_, mul_inv_to_fun_mem hR g⟩)) : finset H) : set H) = ⊤ :=
begin
  rw [finset.coe_image, finset.coe_mul],
  exact closure_mul_image_eq_top hR hR1 hS,
end

variables (H)

lemma exists_finset_card_le_mul [finite_index H] {S : finset G} (hS : closure (S : set G) = ⊤) :
  ∃ T : finset H, T.card ≤ H.index * S.card ∧ closure (T : set H) = ⊤ :=
begin
  letI := H.fintype_quotient_of_finite_index,
  haveI : decidable_eq G := classical.dec_eq G,
  obtain ⟨R₀, hR : R₀ ∈ right_transversals (H : set G), hR1⟩ := exists_right_transversal (1 : G),
  haveI : fintype R₀ := fintype.of_equiv _ (mem_right_transversals.to_equiv hR),
  let R : finset G := set.to_finset R₀,
  replace hR : (R : set G) ∈ right_transversals (H : set G) := by rwa set.coe_to_finset,
  replace hR1 : (1 : G) ∈ R := by rwa set.mem_to_finset,
  refine ⟨_, _, closure_mul_image_eq_top' hR hR1 hS⟩,
  calc _ ≤ (R * S).card : finset.card_image_le
  ... ≤ (R ×ˢ S).card : finset.card_image_le
  ... = R.card * S.card : R.card_product S
  ... = H.index * S.card : congr_arg (* S.card) _,
  calc R.card = fintype.card R : (fintype.card_coe R).symm
  ... = _ : (fintype.card_congr (mem_right_transversals.to_equiv hR)).symm
  ... = fintype.card (G ⧸ H) : quotient_group.card_quotient_right_rel H
  ... = H.index : H.index_eq_card.symm,
end

/-- **Schreier's Lemma**: A finite index subgroup of a finitely generated
  group is finitely generated. -/
instance fg_of_index_ne_zero [hG : group.fg G] [finite_index H] : group.fg H :=
begin
  obtain ⟨S, hS⟩ := hG.1,
  obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS,
  exact ⟨⟨T, hT⟩⟩,
end

lemma rank_le_index_mul_rank [hG : group.fg G] [finite_index H] :
  group.rank H ≤ H.index * group.rank G :=
begin
  haveI := H.fg_of_index_ne_zero,
  obtain ⟨S, hS₀, hS⟩ := group.rank_spec G,
  obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS,
  calc group.rank H ≤ T.card : group.rank_le H hT
  ... ≤ H.index * S.card : hT₀
  ... = H.index * group.rank G : congr_arg ((*) H.index) hS₀,
end

variables (G)

/-- If `G` has `n` commutators `[g₁, g₂]`, then `|G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n + 1)`,
where `G'` denotes the commutator of `G`. -/
lemma card_commutator_dvd_index_center_pow [finite (commutator_set G)] :
  nat.card (commutator G) ∣
    (center G).index ^ ((center G).index * nat.card (commutator_set G) + 1) :=
begin
  -- First handle the case when `Z(G)` has infinite index and `[G : Z(G)]` is defined to be `0`
  by_cases hG : (center G).index = 0,
  { simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero] },
  haveI : finite_index (center G) := ⟨hG⟩,
  -- Rewrite as `|Z(G) ∩ G'| * [G' : Z(G) ∩ G'] ∣ [G : Z(G)] ^ ([G : Z(G)] * n) * [G : Z(G)]`
  rw [←((center G).subgroup_of (commutator G)).card_mul_index, pow_succ'],
  -- We have `h1 : [G' : Z(G) ∩ G'] ∣ [G : Z(G)]`
  have h1 := relindex_dvd_index_of_normal (center G) (commutator G),
  -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n)`
  refine mul_dvd_mul _ h1,
  -- We know that `[G' : Z(G) ∩ G'] < ∞` by `h1` and `hG`
  haveI : finite_index ((center G).subgroup_of (commutator G)) := ⟨ne_zero_of_dvd_ne_zero hG h1⟩,
  -- We have `h2 : rank (Z(G) ∩ G') ≤ [G' : Z(G) ∩ G'] * rank G'` by Schreier's lemma
  have h2 := rank_le_index_mul_rank ((center G).subgroup_of (commutator G)),
  -- We have `h3 : [G' : Z(G) ∩ G'] * rank G' ≤ [G : Z(G)] * n` by `h1` and `rank G' ≤ n`
  have h3 := nat.mul_le_mul (nat.le_of_dvd (nat.pos_of_ne_zero hG) h1) (rank_commutator_le_card G),
  -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ rank (Z(G) ∩ G')`
  refine dvd_trans _ (pow_dvd_pow (center G).index (h2.trans h3)),
  -- `Z(G) ∩ G'` is abelian, so it enough to prove that `g ^ [G : Z(G)] = 1` for `g ∈ Z(G) ∩ G'`
  apply card_dvd_exponent_pow_rank' _ (λ g, _),
  -- `Z(G)` is abelian, so `g ∈ Z(G) ∩ G' ≤ G' ≤ ker (transfer : G → Z(G))`
  have := abelianization.commutator_subset_ker (monoid_hom.transfer_center_pow G) g.1.2,
  -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done
  simpa only [monoid_hom.mem_ker, subtype.ext_iff] using this,
end

/-- A bound for the size of the commutator subgroup in terms of the number of commutators. -/
def card_commutator_bound (n : ℕ) := (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1)

/-- A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of
  commutators. -/
lemma card_commutator_le_of_finite_commutator_set [finite (commutator_set G)] :
  nat.card (commutator G) ≤ card_commutator_bound (nat.card (commutator_set G)) :=
begin
  have h1 := index_center_le_pow (closure_commutator_representatives G),
  have h2 := card_commutator_dvd_index_center_pow (closure_commutator_representatives G),
  rw card_commutator_set_closure_commutator_representatives at h1 h2,
  rw card_commutator_closure_commutator_representatives at h2,
  replace h1 := h1.trans (nat.pow_le_pow_of_le_right finite.card_pos
    (rank_closure_commutator_representations_le G)),
  replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_right (mul_le_mul_right' h1 _) 1)),
  rw ← pow_succ' at h2,
  refine (nat.le_of_dvd _ h2).trans (nat.pow_le_pow_of_le_left h1 _),
  exact pow_pos (nat.pos_of_ne_zero finite_index.finite_index) _,
end

/-- A theorem of Schur: A group with finitely many commutators has finite commutator subgroup. -/
instance [finite (commutator_set G)] : finite (commutator G) :=
begin
  have h2 := card_commutator_dvd_index_center_pow (closure_commutator_representatives G),
  refine nat.finite_of_card_ne_zero (λ h, _),
  rw [card_commutator_closure_commutator_representatives, h, zero_dvd_iff] at h2,
  exact finite_index.finite_index (pow_eq_zero h2),
end

end subgroup
